PRISM
=====
Version: 4.5.dev
Date: Sun Mar 15 00:39:37 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 wlan.6.prism wlan.props --property cost_min -const COL=0
Parsing model file "wlan.6.prism"...
Type: MDP
Modules: medium station1 station2
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Parsing properties file "wlan.props"...
7 properties:
(1) "collisions": Pmax=? [ F col=COL ]
(2) "cost_max": R{"cost"}max=? [ F s1=12&s2=12 ]
(3) "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
(4) "num_collisions": R{"collisions"}max=? [ F s1=12&s2=12 ]
(5) "sent": P>=1 [ F s1=12&s2=12 ]
(6) "time_max": R{"time"}max=? [ F s1=12&s2=12 ]
(7) "time_min": R{"time"}min=? [ F s1=12&s2=12 ]
---------------------------------------------------------------------
Model checking: "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
Model constants: COL=0
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: COL=0
Computing reachable states... 206873 460300 679291 925187 1279717 1611934 1684193 1839325 2114266 2316030 2561062 2603438 2908561 3294497 3684582 4044073 4432011 4824029 5007548 states
Reachable states exploration and model construction done in 56.26 secs.
Sorting reachable states list...
Time for model construction: 62.081 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 3101 iterations and 1123.776 seconds.
target=1, inf=0, rest=5007547
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 1.532 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (1.066 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 25.346 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 441670.8165168762
Starting Prob1 (min)...
----------
Computation aborted after 1800.2914917469025 seconds since the total time limit of 1800 seconds was exceeded.